/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sofia Rodrigues
-/
module

prelude
public import Init.System.Promise
public import Init.Data.SInt
public import Std.Net

public section

namespace Std
namespace Internal
namespace UV

private opaque SignalImpl : NonemptyType.{0}

/--
`Signal`s are used to generate `IO.Promise`s that resolve when a specific signal is received.

A `Signal` can be in one of 3 states:
- Right after construction it's initial.
- While it is listening for signals it's running.
- If it has stopped for some reason it's finished.

This together with whether it was set up as `repeating` with `Signal.mk` determines the behavior
of all functions on `Signal`s.
-/
def Signal : Type := SignalImpl.type

instance : Nonempty Signal := by exact SignalImpl.property

namespace Signal

/--
This creates a `Signal` in the initial state and doesn't start listening yet.
- If `repeating` is `false` this constructs a signal handler that resolves once when the specified
  signal `signum` is received, then automatically stops listening.
- If `repeating` is `true` this constructs a signal handler that resolves each time the specified
  signal `signum` is received and continues listening. A repeating signal handler will only be
  freed after `Signal.stop` is called.
-/
@[extern "lean_uv_signal_mk"]
opaque mk (signum : Int32) (repeating : Bool) : IO Signal

/--
This function has different behavior depending on the state and configuration of the `Signal`:
- if `repeating` is `false` and:
  - it is initial, start listening and return a new `IO.Promise` that is set to resolve once
    the signal `signum` is received. After this `IO.Promise` is resolved the `Signal` is finished.
  - it is running or finished, return the same `IO.Promise` that the first call to `next` returned.
- if `repeating` is `true` and:
  - it is initial, start listening and return a new `IO.Promise` that resolves when the next
    signal `signum` is received.
  - it is running, check whether the last returned `IO.Promise` is already resolved:
     - If it is, return a new `IO.Promise` that resolves upon receiving the next signal
     - If it is not, return the last `IO.Promise`
     This ensures that the returned `IO.Promise` resolves at the next occurrence of the signal.
  - if it is finished, return the last `IO.Promise` created by `next`. Notably this could be one
    that never resolves if the signal handler was stopped before fulfilling the last one.

The resolved `IO.Promise` contains the signal number that was received.
-/
@[extern "lean_uv_signal_next"]
opaque next (signal : @& Signal) : IO (IO.Promise Int)

/--
This function has different behavior depending on the state of the `Signal`:
- If it is initial or finished this is a no-op.
- If it is running the signal handler is stopped and it is put into the finished state.
  Note that if the last `IO.Promise` generated by `next` is unresolved and being waited
  on this creates a memory leak and the waiting task is not going to be awoken anymore.
-/
@[extern "lean_uv_signal_stop"]
opaque stop (signal : @& Signal) : IO Unit

/--
This function has different behavior depending on the state of the `Signal`:
- If it is initial or finished this is a no-op.
- If it's running then it drops the accept promise and if it's not repeatable it sets
  the signal handler to the initial state.
-/
@[extern "lean_uv_signal_cancel"]
opaque cancel (signal : @& Signal) : IO Unit

end Signal

end UV
end Internal
end Std
